Nuprl Definition : sumdeq
11,40
postcript
pdf
sumdeq(
a
;
b
)(
p
,
q
)
== case
p
==
of inl(
pa
) => case
q
of inl(
qa
) => (
a
.1)(
pa
,
qa
) | inr(
qb
) => ff
== o
| inr(
pb
) => case
q
of inl(
qa
) => ff | inr(
qb
) => (
b
.1)(
pb
,
qb
)
latex
Definitions
t
.1
,
ff
FDL editor aliases
sumdeq
origin